ds1, ds2:x:Id fp Type, da1, da2:k:Knd fp Type.
ds2  ds1  da2  da1  ecl(ds2;da2)  ecl(ds1;da1) 

latex

Definitions	x:A. B(x), P  Q, ecl(ds;da), t  T, eclbase(k;test), x. t(x), S  T, S  T, State(ds), x(s), eclseq(a;b), ecland(a;b), eclor(a;b), [a]*, a.n, eclthrow(a;n), eclcatch(a;l), Prop, State(ds)
Lemmas	eclseq wf, ecland wf, eclor wf, eclrepeat wf, eclact wf, eclthrow wf, eclcatch wf, ecl wf, fpf-sub wf, Knd wf, Kind-deq wf, Id wf, id-deq wf, fpf wf, eclbase wf, ma-state-subtype, ma-state wf, ma-valtype-subtype